
The Knaster-Tarski theorem: proof
Proof.
We write C = {X ∈ P(U) | F (X ) ⊆ X }.
Given X ∈ C, we have fix(F ) =
T
C ⊆ X (*)
and therefore, since F is increasing, F (fix(F )) ⊆ F (X ) ⊆ X (**)
from which we deduce F (fix(F )) ⊆
T
C = fix(F).
Moreover, by monotonicity again, we have F (F (fix(F ))) ⊆ F (fix(F ))
therefore, F (fix(F )) ∈ C,
and thus, by (*), fix(F ) ⊆ F (fix(F ))
We have shown that fix(F ) is a fixpoint of F .
Given a fixpoint X of F , we have X ∈ C
thus, by (**), fix(F ) = F (fix(F )) ⊆ X
i.e. fix(F ) is the smallest fixpoint.
84